home *** CD-ROM | disk | FTP | other *** search
/ PC-Blue - MS DOS Public Domain Library / PC-Blue MS-DOS Public Domain Library - NYACC.iso / vol350 / prolog.arc / CAD.ARC / DREXATGS.ARC / ATGS.PRO < prev    next >
Encoding:
Text File  |  1987-04-05  |  15.0 KB  |  515 lines
  1. /*
  2. .pn1
  3. .he                           DREXEL ATGS */ 
  4.  
  5. constrainlist( [constraint1] ).
  6.  
  7. constraint1( pc_inv, pdcfinv, pcinv ).
  8. buf(  pc_buf,  pdcfbuf,  pcbuf ).
  9. and2( pc_and2, pdcfand2, pcand2 ).
  10. and3( pc_and3, pdcfand3, pcand3 ).
  11. or2( pc_or2, pdcfor2, pcor2 ).
  12. or3( pc_or3, pdcfor3, pcor3 ).
  13.  
  14. /* The primitive cubes of the logic elements.
  15. Form: pc_type( output, [list of prime implicants] ). */
  16.  
  17. pc_inv( 0, [[1]] ).
  18. pc_inv( 1, [[0]] ).
  19. pc_buf( 0, [[0]] ).
  20. pc_buf( 1, [[1]] ).
  21. pc_and2( 0, [[0,_],[_,0]] ).
  22. pc_and2( 1, [[1,1]] ).
  23. pc_and3( 0, [[0,_,_],[_,0,_],[_,_,0]] ).
  24. pc_and3( 1, [[1,1,1]] ).
  25.  
  26. pc_or2( 1, [[1,_],[_,1]] ).
  27. pc_or2( 0, [[0,0]] ).
  28. pc_or3( 1, [[1,_,_],[_,1,_],[_,_,1]] ).
  29. pc_or3( 0, [[0,0,0]] ).
  30.  
  31.  
  32. /* The primitive D-cubes of the logic elements: */
  33.  
  34. pdcfinv(  sa0(_), db, [[1]] ).
  35. pdcfinv(  sa1(_), d,  [[0]] ).
  36. pdcfbuf(  sa0(_), d,  [[1]] ).
  37. pdcfbuf(  sa1(_), db, [[0]] ).
  38. pdcfand2( sa0(_), d,  [[1,1]] ).
  39. pdcfand2( sa1(1), db, [[0,1]] ).
  40. pdcfand2( sa1(2), db, [[1,0]] ).
  41. pdcfand3( sa0(_), d,  [[1,1,1]] ).
  42. pdcfand3( sa1(1), db, [[0,1,1]] ).
  43. pdcfand3( sa1(2), db, [[1,0,1]] ).
  44. pdcfand3( sa1(3), db, [[1,1,0]] ).
  45.  
  46. pdcfor2( sa0(1), d, [[1,0]] ).
  47. pdcfor2( sa0(2), d, [[0,1]] ).
  48. pdcfor2( sa1(_), db, [[0,0]] ).
  49.  
  50. pdcfor3( sa0(1), d, [[1,0,0]] ).
  51. pdcfor3( sa0(2), d, [[0,1,0]] ).
  52. pdcfor3( sa0(3), d, [[0,0,1]] ).
  53. pdcfor3( sa1(_), db, [[0,0,0]] ).
  54.  
  55. /* The propagation D-cubes of the logic elements: */
  56.  
  57. pcinv( d,  [[db]] ).
  58. èpcinv( db, [[d]] ).
  59. pcbuf( d, [[d]] ).
  60. pcbuf( db, [[db]] ).
  61. pcand2( d, [[1,d],[d,1],[d,d]] ). 
  62. pcand2( db,[[1,db],[db,1],[db,db]] ).
  63. pcor2( d, [[0,d],[d,0,],[d,d]] ).
  64. pcor2( db, [[0,db],[db,0],[db,db]] ).
  65. pcand3( d, 
  66.   [[d,1,1],[1,d,1],[1,1,d],[d,d,1],[d,1,d],[1,d,d],[d,d,d]] ).
  67. pcand3( db,
  68.   [[db,1,1],[1,db,1],[1,1,db],[db,db,1],[db,1,db],[1,db,db],[db,db,db]] ).
  69. pcor3( d,
  70.   [[d,0,0],[0,d,0],[0,0,d],[d,d,0],[d,0,d],[0,d,d],[d,d,d]] ).
  71. pcor3( db,
  72.   [[db,0,0],[0,db,0],[0,0,db],[db,db,0],[db,0,db],[0,db,db],[db,db,db]] ).
  73.  
  74.  
  75. /* Samples:
  76. Type:      and3( pdcfand3, pcand3 ).
  77. Pdcfclass: pdcfand3( sa1(3), db, [[1,1,0]] ).
  78. Gate:      r6( or3, 3, [n25,n26,n28], n34 ).
  79. */
  80.  
  81. /* Gatelines = [ [x,x,x], [x,x,x],..., [x,x,x] ] */
  82. /* Netnames =  [ nx(val), .... nx(val) ] */
  83.  
  84.  
  85.  
  86. /*
  87.    Netvals = current assignments of nets: [n1(1), n5(0),.....,nn(x)]
  88.    Inputnets = input nets to specific gate: [n1,n3,..nx]
  89.    Inputvals = [1,0,.d, db, 0]
  90. */
  91.  
  92.  
  93.  
  94.  
  95. listsubt( [], _, Res, Res ).
  96. listsubt( [Head|Mainlist], El, Buildlist, Result ) :-
  97.     (Head == El, listsubt( Mainlist, El, Buildlist, Result ));
  98.     listsubt( Mainlist, El, [Head|Buildlist], Result ), !.
  99.  
  100. findouttests( Gate, Fault ) :- 
  101.     print('\nSynthesizing Output Tests for: ', Gate, ' Fault: ', Fault ),
  102.     memleft( Memleft1 ),
  103.         print( '\nMemleft start gen: ', Memleft1 ),
  104.     (ftout( Gate, Fault ); true), 
  105.         !.
  106.  
  107. ftout( Gate, Fault ) :-
  108.     gentestoutp( Gate, Fault, TestInputs, TestOutputs ),
  109.     asserta( test( Gate, output, Fault, TestInputs, TestOutputs ) ),
  110.     print( '\n  Testinputs:  ', TestInputs ),
  111.     print( '\n  Testoutputs: ', TestOutputs ),
  112.     !,
  113. è        fail.
  114.  
  115.  
  116. findinptests( Gate, Input, Fault ) :- 
  117.     print('\nSynthesizing Input Tests for: ', Gate, ', Input: ', Input,
  118.              ' Fault: ', Fault ),
  119.     (ftinp( Gate, Input, Fault ); true), !.
  120.  
  121.  
  122. ftinp( Gate, Input, Fault ) :-
  123.     gentestinp( Gate, Input, Fault, TestInputs, TestOutputs ),
  124.     print( '\n  Testinputs:  ', TestInputs ),
  125.     print( '\n  Testoutputs: ', TestOutputs ), 
  126.     asserta( test( Gate, Input, Fault, TestInputs, TestOutputs ) ),
  127.         !,
  128.     fail.
  129.  
  130. /*
  131. ftinp( Gate, Input, Fault ) :-
  132.     !,
  133.     test( Gate, Input, Fault, TestInputs, TestOutputs ),
  134.     print( '\n  Testinputs:  ', TestInputs ),
  135.     print( '\n  Testoutputs: ', TestOutputs ),
  136.     fail.
  137. */
  138.  
  139.  
  140. gentestoutp( Gate, Fault, TestInputs, TestOutputs ) :-
  141.     Gate( Type, _, Inplist, Outnet ),
  142.     Type( Primcube, _, _ ),
  143.     elements( Ellist ),
  144.       listsubt( Ellist, Gate, [], Sublist ), !,
  145.     (
  146.           (
  147.             Fault == sa0, 
  148.         Primcube( 1, Implicants ),
  149.             member( Implicant, Implicants ),
  150.             pairoff( Inplist, Implicant, [], Netvals ),
  151.             ad_vals_to_Net( [Outnet(d)], Netvals, NNetvals )
  152.           );
  153.           (
  154.         Fault == sa1, 
  155.         Primcube( 0, Implicants ),
  156.             member( Implicant, Implicants ),
  157.             pairoff( Inplist, Implicant, [], Netvals ),
  158.             ad_vals_to_Net( [Outnet(db)], Netvals, NNetvals )
  159.       )
  160.         ),
  161.     outputs( Outlist ),
  162.     ( 
  163.           (
  164.             member( Outnet, Outlist ),
  165.             imply1( NNetvals, Sublist, NNNetvals, Undef ),
  166.             justify( NNNetvals, Undef, NNNNetvals ),
  167.             getinps( NNNNetvals, TestInputs ),
  168. è        getoutp( NNNNetvals, TestOutputs )
  169.           );
  170.           (
  171.             not( member( Outnet, Outlist ) ),
  172.             propagate( NNetvals, Sublist, 
  173.                                   NNNetvals, Undef, Solved ),
  174.             Solved == true,
  175.             justify( NNNetvals, Undef, NNNNetvals ),
  176.             getinps( NNNNetvals, TestInputs ),
  177.             getoutp( NNNNetvals, TestOutputs )
  178.           )
  179.         ).
  180.  
  181.  
  182.  
  183. gentestinp( Gate, Input, Fault, TestInputs, TestOutputs ) :-
  184.         Gate( Type, _, Inplist, Outnet ),
  185.         Type( _, Pdcfclass, _ ),
  186.         elements( Ellist ),
  187.         listsubt( Ellist, Gate, [], Sublist ),
  188.         !,
  189.     Pdcfclass( Fault(Input), Dtype, Implicants ),
  190.     member( Implicant, Implicants ),
  191.     pairoff( Inplist, Implicant, [], Netvals ),
  192.         outputs( Outlist ),
  193.         ( 
  194.           (
  195.             member( Outnet, Outlist ),
  196.             imply1( [Outnet(Dtype)|Netvals], Sublist, NNetvals, Undef ),
  197.             justify( NNetvals, Undef, NNNetvals ),
  198.             getinps( NNNetvals, TestInputs ),
  199.         getoutp( NNNetvals, TestOutputs )
  200.           );
  201.           (
  202.             not( member( Outnet, Outlist ) ),
  203.             propagate( [Outnet(Dtype)|Netvals], Sublist, 
  204.                                   NNetvals, Undef, Solved ),
  205.             Solved == true,
  206.             justify( NNetvals, Undef, NNNetvals ),
  207.             getinps( NNNetvals, TestInputs ),
  208.             getoutp( NNNetvals, TestOutputs )
  209.           )
  210.         ).
  211.  
  212. testfanouts :- testf; true.
  213.  
  214. testf :- 
  215.     findfanoutpts( Fans ), !,
  216.     print('\nElements with fanout:\n  ', Fans ),
  217.     member( Gate, Fans ),
  218.         memleft( Memleft1 ),
  219.         print( '\nMemleft start gen: ', Memleft1 ),
  220.     findouttests( Gate, sa0 ),
  221.         memleft( Memleft2 ),
  222.         print( '\nMemleft after sa0: ', Memleft2 ),
  223. è    findouttests( Gate, sa1 ),
  224.         memleft( Memleft3 ),
  225.         print( '\nMemleft after sa1: ', Memleft3 ),
  226.     fail.
  227.  
  228.  
  229. findfanoutpts( Netswfan ) :-
  230.     elements( Ellist ),
  231.     constrainlist( Constlist ),
  232.     ffo( Ellist, Constlist, [], Netswfan ), !.
  233.  
  234. ffo( [], _, Netform, Netform ).
  235. ffo( [El|Rem], Constlist, Netform, NetRet ) :-
  236.     (
  237.           El( Type, _, _, Outnet ),
  238.       not( member( Type, Constlist ) ),
  239.       Outnet( _, _, Inputlist ),
  240.           [H|T] = Inputlist, T \= [],
  241.       ffo( Rem, Constlist, [El|Netform], NetRet )
  242.         );
  243.     ffo( Rem, Constlist, Netform, NetRet ).
  244.  
  245. testoutputs :- testo ; true.
  246.  
  247. testo :- 
  248.     findoutputs( Outputs ), !,
  249.     member( Gate, Outputs ),
  250.         memleft( Memleft1 ),
  251.         print( '\nMemleft start gen: ', Memleft1 ),
  252.     findouttests( Gate, sa0 ),
  253.         memleft( Memleft2 ),
  254.         print( '\nMemleft after sa0: ', Memleft2 ),
  255.     findouttests( Gate, sa1 ),
  256.         memleft( Memleft3 ),
  257.         print( '\nMemleft after sa1: ', Memleft3 ),
  258.     fail.
  259.  
  260.  
  261.  
  262.  
  263. findoutputs( Netswfan ) :-
  264.     elements( Ellist ),
  265.     outputs( Outputs ),
  266.     fout( Ellist, Outputs, [], Netswfan ), !.
  267.  
  268. fout( [], _, Netform, Netform ).
  269. fout( [El|Rem], Outputs, Netform, NetRet ) :-
  270.     (
  271.           El( Type, _, _, Outnet ),
  272.           member( Outnet, Outputs ),
  273.       fout( Rem, Outputs, [El|Netform], NetRet )
  274.         );
  275.     fout( Rem, Outputs, Netform, NetRet ).
  276.  
  277. testinputs :- testi ; true.
  278. è
  279. testi :- 
  280.     findinputs( Inputs ), !,
  281.     member( [Gate,Input], Inputs ),
  282.         memleft( Memleft1 ),
  283.         print( '\nMemleft start gen: ', Memleft1 ),
  284.     findinptests( Gate, Input, sa0 ),
  285.         memleft( Memleft2 ),
  286.         print( '\nMemleft after sa0: ', Memleft2 ),
  287.     findinptests( Gate, Input, sa1 ),
  288.         memleft( Memleft3 ),
  289.         print( '\nMemleft after sa1: ', Memleft3 ),
  290.     fail.
  291.  
  292. findinputs( InpEls ) :-
  293.     elements( Ellist ),
  294.     inputs( Inputs ),
  295.     finp( Inputs, [], InpEls ), !.
  296.  
  297. finp( [], Netform, Netform ).
  298. finp(  [Inputnet|InpnetRem], Netform, NetRet ) :-
  299.     (
  300.           Inputnet( _, _, [El|_] ),
  301.           El( _, _, Nets, _ ),
  302.           member( Inputnet, Nets, Num ),
  303.           Numplus is Num + 1,
  304.       finp( InpnetRem, [[El,Numplus]|Netform], NetRet )
  305.         );
  306.     finp( ElRem, InpnetRem, Netform, NetRet ).
  307.  
  308.  
  309.  
  310. justify( Netvals, [], Netvals ).
  311. justify( Netvals, [El|Rem], NewNetReturn ) :-
  312.     El( Type, _, Inputs, Outnet ),
  313.         replcbyval( Netvals, Inputs, Vals, Varlist ),
  314.         Type( Pc, _, _ ),
  315.         (
  316.           (
  317.             member( Outnet(Output), Netvals ), 
  318.             !,
  319.             Pc( Output, Implicants ), 
  320.  
  321.             member( Implicant, Implicants ),
  322.  
  323.             Implicant = Vals,
  324.             ad_vals_to_Net( Netvals, Varlist, NNetvals ),
  325.         imply1( NNetvals, Rem, NNNewNet, Undef ),
  326.         justify( NNNewNet, Undef, NewNetReturn )
  327.           );
  328.       (
  329.             not( member( Outnet(Output), Netvals ) ),
  330.             justify( Netvals, Rem, NewNetReturn )
  331.           ) 
  332.         ).
  333. è
  334.  
  335.  
  336.  
  337.  
  338. propagate( Netvals, [], Netvals, [], _ ).
  339. propagate( Netvals, Ellist, NNNNetvals, UndefR, Solved ) :-
  340.     usecount(U),
  341.     imply1( Netvals, Ellist, NNetvals, UndefEllist ),
  342.     ddrive( NNetvals, UndefEllist, NNNetvals, [], 
  343.                               UndefEllist2, Solved, Drive  ),
  344.         (
  345.           (Solved == true, NNNNetvals = NNNetvals, UndefR = UndefEllist2, !); 
  346.           (
  347.             Drive == true,
  348.             propagate( NNNetvals, UndefEllist2, NNNNetvals, UndefR, Solved )
  349.           )
  350.         ).
  351.  
  352. /* Here [] is the empty list of elements currently in the D-frontier. */
  353.  
  354.  
  355.  
  356.  
  357. ddrive( Netvals, [], Netvals, Undef, UndefR, _, _  ) :-
  358.     revlist( Undef, UndefR ).
  359. ddrive( Netvals, [El|Remain], ReturnNewNet, Undefform, 
  360.                   Undefreturn, Solved, Drive ) :-
  361.     usecount(U),
  362.     El( Type, _, Inputs, Outnet ),
  363.     ( 
  364.           (
  365.         replcbyval( Netvals, Inputs, Vals, Varlist ),
  366.             hasD( Vals ),
  367.             Type( _, _, Prcube ),
  368.             Prcube( Output, Implicants ), 
  369.             member( Implicant, Implicants ), 
  370.             Implicant = Vals,
  371.             ad_vals_to_Net( Netvals, Varlist, NNetvals ),
  372.             notdup( Outnet, Output, Netvals, NNetvals, NNNetvals ),
  373.         Drive = true,
  374.             (
  375.               (
  376.                 outputs( Outlist ), 
  377.                 member( Outnet, Outlist ),
  378.             Solved = true, !,
  379.                 ReturnNewNet = NNNetvals,
  380.                 revlist( Undefform, UdfR ),
  381.                 appenddef( UdfR, Remain, Undefreturn )
  382.               );    
  383.               ddrive( NNNetvals, Remain, ReturnNewNet, 
  384.                           Undefform, Undefreturn, Solved, Drive  )
  385.             )
  386.           );(
  387.           ddrive( Netvals, Remain, ReturnNewNet, 
  388. è                            [El|Undefform], Undefreturn, Solved, Drive  ))
  389.         ).
  390.  
  391.  
  392.  
  393. hasD( Inputs ) :- vmember( d, Inputs ); vmember( db, Inputs ).
  394.  
  395.  
  396. imply1( Netvals, Ellist, NNetvals, UndefEllist2 ) :-
  397.     imply( Netvals, Ellist, NNetvals, [], UndefEllist ),     
  398.     revlist( UndefEllist, UndefEllist2 ),
  399.     !.
  400.  
  401. imply( NewNetvals, [], NewNetvals, Undef, Undef ).
  402.  
  403. imply( Netvals, [El|Remain], ReturnNewNet, Undefform, Undefreturn ) :-
  404.         usecount(U),
  405.     El( Type, _, Inputs, Outnet ),
  406.         ( 
  407.           (
  408.           replcbyval( Netvals, Inputs, Vals, Varlist ),
  409.           not( hasD( Vals ) ),
  410.           Type( Pc, _, _ ),
  411.           Pc( Output, Implicants ), 
  412.           member( Implicant, Implicants ), 
  413.           Implicant == Vals,
  414.           notdup( Outnet, Output, Netvals, Netvals, NNNetvals ),
  415.           imply( NNNetvals, Remain, ReturnNewNet, Undefform, Undefreturn)
  416.           );
  417.           imply( Netvals, Remain, ReturnNewNet, [El|Undefform], Undefreturn) 
  418.         ).
  419.  
  420. notdup( Netval, Val, Netvals, NNetvals, NNetvals ) :-
  421.     member( Netval(Extval), Netvals ),
  422.     !,
  423.     Extval == Val.
  424.     
  425. notdup( Netval, Val, _, NNetvals, [Netval(Val)|NNetvals] ) :- !.
  426.  
  427.  
  428. ad_vals_to_Net( Netvals, Varlist, NewNet ) :-
  429.     advals( Netvals, Varlist, NewNet ), !.
  430. advals( Netvals, [], Netvals ).
  431. advals( Netvals, [Head(Val)|Varlist], NNetvalsR ) :-
  432.     (
  433.           (
  434.             atomic(Val),
  435.         advals( [Head(Val)|Netvals], Varlist, NNetvalsR )
  436.           );
  437.           advals( Netvals, Varlist, NNetvalsR )
  438.         ).
  439.  
  440.  
  441. /*
  442.    Netvals = current assignments of nets: [n1(1), n5(0),.....,nn(x)]
  443. è   Inputnets = input nets to specific gate: [n1,n3,..nx]
  444.    Inputvals = [1,0,.d, db, 0]
  445. */
  446.  
  447. replcbyval( A, B, C, NetVarlist) :- 
  448.                            replcbyval1( A, B, C, [], NetVarlist ), !.
  449.  
  450. replcbyval1( _, [], [], NetVarlist, NetVarlist ).
  451. replcbyval1( Netvals, [Inputnet|Restnets], 
  452.               [Inputval|Restvals], NetVarlist, NetVarR ) :-
  453.     (
  454.           (
  455.             member( Inputnet( Inputval ), Netvals ), 
  456.             NetVarT = NetVarlist
  457.           );
  458.           (
  459.             var( Inputval ),
  460.             NetVarT = [Inputnet(Inputval)|NetVarlist]
  461.           )
  462.         ),
  463.     replcbyval1( Netvals, Restnets, Restvals, NetVarT, NetVarR ).
  464.  
  465. getinps( A, B ) :- 
  466.     inputs( Inplist ),
  467.     getinps1( A, Inplist, [], B ), !, Inplist \= [].
  468.  
  469. getinps1( _, [], Netandvals, Netandvals ).
  470. getinps1( Netvals, [Inputnet|Restnets], Inplistform, Retlist ) :-
  471.     (
  472.           member( Inputnet( Inputval ), Netvals ), 
  473.       getinps1( Netvals, Restnets, 
  474.                    [Inputnet(Inputval)|Inplistform], Retlist )
  475.         );
  476.     getinps1( Netvals, Restnets, Inplistform, Retlist ).
  477.  
  478. getoutp( A, B ) :- 
  479.     outputs( Outplist ),
  480.     getoutp1( A, Outplist, [], B ), !, Outplist \= [].
  481.  
  482. getoutp1( _, [], Netandvals, Netandvals ).
  483. getoutp1( Netvals, [Outputnet|Restnets], Outlistform, Retlist ) :-
  484.     (
  485.           member( Outputnet( Outputval ), Netvals ), 
  486.           (Outputval == d ; Outputval == db),
  487.       getoutp1( Netvals, Restnets, 
  488.                    [Outputnet(Outputval)|Outlistform], Retlist )
  489.         );
  490.     getoutp1( Netvals, Restnets, Outlistform, Retlist ).
  491.  
  492.  
  493.  
  494.  
  495.  
  496. /* funclist = [nx,...,nx],    arglist = [1,0,...,etc] */
  497. pairoff( [], [], Result, Result ).
  498. èpairoff( [Func|F_rem], [Arg|Arg_rem], Tlist, Reslist ) :-
  499.     pairoff( F_rem, Arg_rem, [Func(Arg)|Tlist], Reslist ).
  500.  
  501.  
  502. /* Samples:
  503. Type:      and3( pdcfand3, pcand3 ).
  504. Pdcfclass: pdcfand3( sa1(3), db, [[1,1,0]] ).
  505. Gate:      r6( or3, 3, [n25,n26,n28], n34 ).
  506. */
  507.  
  508. appenddef( L1, L2, L3 ) :- append( L1, L2, L3 ), !.
  509. append([],L,L).
  510. append([Z|L1],L2,[Z|L3]) :- append( L1,L2,L3 ).
  511.  
  512.  
  513. /* Non-instantiating member, for lists containing variables: */
  514. vmember( X, List ) :- member( Y, List ), X == Y, !.
  515.  
  516.  
  517.  
  518. revlist( List, Reverse ) :- rev( List, [], Reverse ), !.
  519. rev( [], L, L ).
  520. rev( [H|List], Formlist, Retlist ) :-
  521.     rev( List, [H|Formlist], Retlist ).
  522.  
  523.  
  524.